$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $m$:$\mathbb{N}$, $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$).
\\[0ex]add{-}ecl{-}act($A$;$m$) $\in$ ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$)